Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    sort(nil)  → nil
2:    sort(cons(x,y))  → insert(x,sort(y))
3:    insert(x,nil)  → cons(x,nil)
4:    insert(x,cons(v,w))  → choose(x,cons(v,w),x,v)
5:    choose(x,cons(v,w),y,0)  → cons(x,cons(v,w))
6:    choose(x,cons(v,w),0,s(z))  → cons(v,insert(x,w))
7:    choose(x,cons(v,w),s(y),s(z))  → choose(x,cons(v,w),y,z)
There are 5 dependency pairs:
8:    SORT(cons(x,y))  → INSERT(x,sort(y))
9:    SORT(cons(x,y))  → SORT(y)
10:    INSERT(x,cons(v,w))  → CHOOSE(x,cons(v,w),x,v)
11:    CHOOSE(x,cons(v,w),0,s(z))  → INSERT(x,w)
12:    CHOOSE(x,cons(v,w),s(y),s(z))  → CHOOSE(x,cons(v,w),y,z)
The approximated dependency graph contains 2 SCCs: {10-12} and {9}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.22 seconds)   ---  May 4, 2006